Nuprl Lemma : es-realizer_wf 0,22

P:(ES{i}Prop{i'}), p:es-real{i:l}(es.P(es)). es-realizer(p es_realizer{i:l} 
latex


Definitionsx:AB(x), Prop, x(s), t  T, es-realizer(p), 1of(t), xt(x), es.P(es), x:AB(x)
Lemmases-real wf, event system wf

origin